Nuprl Lemma : es-pstar-q_functionality_wrt_rev_implies 0,22
es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, p', q', p,
q:({e:E| loc(e) = loc(e1)  Id }{e:E| loc(e) = loc(e1)  Id }Prop).
(a, b:{e:E| loc(e) = loc(e1)  Id }. (a  [e1, e2])  (b  [e1, e2])  {p(a,b)  p'(a,b)})
 (a, b:{e:E| loc(e) = loc(e1)  Id }. (a  [e1, e2])  (b  [e1, e2])  {q(a,b)  q'(a,b)})
 {[e1;e2]~([a,b].p(a,b))*[a,b].q(a,b)  [e1;e2]~([a,b].p'(a,b))*[a,b].q'(a,b)} 
latex

DefinitionsP  Q
Lemmases-pstar-q functionality wrt implies

origin